\begin{tabbing}
$\forall$\=${\it es}$:ES, $A$:Type, $l$:IdLnk, ${\it tg}$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type,\+
\\[0ex]${\it conds}$:$k$:Knd fp$\rightarrow$ $V$:Type $\times$ (State(${\it ds}$)$\rightarrow$$V$$\rightarrow$($A$ + Top)).
\-\\[0ex]($\forall$$k$:Knd. ($\uparrow$$k$ $\in$ dom(${\it conds}$)) $\Rightarrow$ ($\uparrow$hasloc($k$;source($l$))))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. (kind($e$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ (valtype($e$) $\subseteq$r $A$))
\\[0ex]$\Rightarrow$ \=($\forall$$k$:Knd.\+
\\[0ex]($\uparrow$$k$ $\in$ dom(${\it conds}$))
\\[0ex]$\Rightarrow$ \=$k$(v:${\it conds}$($k$).1) sends on $l$ [${\it tg}$:$A$, $\lambda$$p$.let $s$,$v$ = $p$\+
\\[0ex]in
\\[0ex](${\it conds}$($k$).2)($s$,$v$) $<$state, v$>$]?[])
\-\-\\[0ex]$\Rightarrow$ only events in fpf{-}domain(${\it conds}$) send on $l$ with ${\it tg}$
\\[0ex]$\Rightarrow$ glues(\=${\it es}$;\+
\\[0ex]$A$;
\\[0ex]($\lambda$$e$.sender($e$));
\\[0ex]($\lambda$$e$.outl((${\it conds}$(kind($e$)).2)((state when $e$),val($e$))));
\\[0ex]es{-}triggers(${\it es}$;source($l$);${\it ds}$;${\it conds}$);
\\[0ex]es{-}in{-}port(${\it es}$;$l$;${\it tg}$))
\-
\end{tabbing}